Problem:
 p(0(x1)) -> 0(s(s(p(x1))))
 p(s(x1)) -> x1
 p(p(s(x1))) -> p(x1)
 f(s(x1)) -> p(s(g(p(s(s(x1))))))
 g(s(x1)) -> p(p(s(s(s(j(s(p(s(p(s(x1)))))))))))
 j(s(x1)) -> p(s(s(p(s(f(p(s(p(p(s(x1)))))))))))
 half(0(x1)) -> 0(s(s(half(p(s(p(s(x1))))))))
 half(s(s(x1))) -> s(half(p(p(s(s(x1))))))
 rd(0(x1)) -> 0(s(0(0(0(0(s(0(rd(x1)))))))))

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {8,7,6,5,4,3}
   transitions:
    01(107) -> 108*
    01(102) -> 103*
    01(12) -> 13*
    01(109) -> 110*
    01(104) -> 105*
    01(106) -> 107*
    01(86) -> 87*
    01(105) -> 106*
    s1(85) -> 86*
    s1(80) -> 81*
    s1(10) -> 11*
    s1(77) -> 78*
    s1(47) -> 48*
    s1(42) -> 43*
    s1(27) -> 28*
    s1(99) -> 100*
    s1(84) -> 85*
    s1(79) -> 80*
    s1(74) -> 75*
    s1(44) -> 45*
    s1(39) -> 40*
    s1(24) -> 25*
    s1(46) -> 47*
    s1(11) -> 12*
    s1(108) -> 109*
    s1(103) -> 104*
    s1(48) -> 49*
    s1(23) -> 24*
    rd1(101) -> 102*
    rd1(123) -> 124*
    half1(98) -> 99*
    half1(83) -> 84*
    p1(75) -> 76*
    p1(50) -> 51*
    p1(25) -> 26*
    p1(97) -> 98*
    p1(49) -> 50*
    p1(9) -> 10*
    p1(81) -> 82*
    p1(41) -> 42*
    p1(21) -> 22*
    p1(78) -> 79*
    p1(73) -> 74*
    p1(43) -> 44*
    p1(28) -> 29*
    f1(76) -> 77*
    j1(45) -> 46*
    g1(26) -> 27*
    p2(187) -> 188*
    p2(157) -> 158*
    p2(154) -> 155*
    p2(149) -> 150*
    p2(186) -> 187*
    p2(151) -> 152*
    p2(163) -> 164*
    p2(133) -> 134*
    p2(180) -> 181*
    p2(160) -> 161*
    p2(155) -> 156*
    p2(135) -> 136*
    p0(2) -> 3*
    p0(1) -> 3*
    s2(162) -> 163*
    s2(184) -> 185*
    s2(179) -> 180*
    s2(159) -> 160*
    s2(181) -> 182*
    s2(161) -> 162*
    s2(156) -> 157*
    s2(183) -> 184*
    s2(153) -> 154*
    s2(185) -> 186*
    00(2) -> 1*
    00(1) -> 1*
    f2(158) -> 159*
    s0(2) -> 2*
    s0(1) -> 2*
    j2(182) -> 183*
    f0(2) -> 4*
    f0(1) -> 4*
    p3(212) -> 213*
    p3(207) -> 208*
    p3(177) -> 178*
    p3(209) -> 210*
    p3(206) -> 207*
    p3(191) -> 192*
    p3(215) -> 216*
    g0(2) -> 5*
    g0(1) -> 5*
    s3(214) -> 215*
    s3(211) -> 212*
    s3(213) -> 214*
    s3(208) -> 209*
    s3(205) -> 206*
    j0(2) -> 6*
    j0(1) -> 6*
    f3(210) -> 211*
    half0(2) -> 7*
    half0(1) -> 7*
    p4(217) -> 218*
    rd0(2) -> 8*
    rd0(1) -> 8*
    1 -> 218,208,178,156,150,74,10,123,39,3,21
    2 -> 218,208,178,156,150,74,10,101,23,3,9
    13 -> 218,208,178,156,136,74,22,10,3
    22 -> 10*
    23 -> 152,149,42,73
    24 -> 151,26,97,41
    26 -> 97*
    27 -> 29*
    29 -> 211,213,159,161,77,79,4
    39 -> 152,135,42,73
    40 -> 24*
    42 -> 44,73
    44 -> 153,83
    47 -> 134,51,5
    48 -> 133,50
    51 -> 5*
    74 -> 76*
    77 -> 79*
    80 -> 82,6
    82 -> 6*
    87 -> 99,84,7
    100 -> 99,84,7
    110 -> 124,102,8
    124 -> 102*
    134 -> 51,5
    136 -> 74*
    150 -> 74*
    152 -> 98*
    153 -> 177,155
    155 -> 179*
    156 -> 158*
    159 -> 161*
    162 -> 164*
    164 -> 46*
    178 -> 156*
    179 -> 181*
    181 -> 205*
    184 -> 192,188
    185 -> 191,187
    188 -> 27,29,4
    192 -> 188*
    205 -> 217,207
    208 -> 210*
    211 -> 213*
    214 -> 216,183
    216 -> 183*
    218 -> 208*
  problem:
   
  Qed